{-# LANGUAGE GADTs, FlexibleContexts, ViewPatterns, FlexibleInstances,
  MultiParamTypeClasses, UndecidableInstances, TemplateHaskell,
  TypeFamilies #-}

module Examples.Eq where

import Data.Yoko



data EqU dc where EqU :: (Generic dc, Eq (RMI (Rep dc))) => EqU dc
obvious_membership ''EqU

instance SetModel EqU where evidence EqU x = x

eqU :: EqU dc -> RMNI dc -> RMNI dc -> Bool
eqU EqU x y = rep x == rep y

gEq :: (DT t, DCs t :=> EqU) => t -> t -> Bool
gEq (disband -> NP u x) (disband -> NP (eqT u -> Just Refl) y) =
  eqU (weaken u) x y
gEq _ _ = False
